MA:MsgA, s:MA.state, k:Knd, l:IdLnk, vaal:MA.V(k).
((MA sends on link l))  (filter(ms.eqof(IdLnkDeq)(mlnk(ms),l);MA.sends(k,s,vaal)) ~ []) 

latex

Definitions	x:A. B(x), P  Q, t  T, x  dom(f), t.1, t.2, S  T, A, x. t(x), (x  l), x:A. B(x), A c B, , P  Q, P  Q, P & Q, {i..j}, i  j < k, MsgA, M.state, M.V(k), M sends on link l, a:A fp B(a), Valtype(da;k), False, x(s),
Lemmas	ma-send-val-nil, not wf, assert wf, ma-sends-on wf, ma-v wf, IdLnk wf, Knd wf, ma-st wf, msga wf, Kind-deq wf, deq-member wf, product-deq wf, idlnk-deq wf, assert-deq-member, map wf, pi2 wf, length wf1, select wf, map length, map select, le wf